i:Id. msg-spec-loc(;i)  True 

latex

Definitions	Id, t  T, True, x:A  B(x), IdLnk, type List, [], x:A. B(x), (x  l), s = t, {T}, P  Q, SQType(T), , ||as||, s ~ t, False, A, A  B, , {x:A| B(x)} , , A c B, x:A. B(x), x:AB(x), xL. P(x), P  Q, source(l), x. t(x), P & Q, P  Q, msg-spec-links(snd), msg-spec-loc(snd;i)
Lemmas	l all wf, lsrc wf, IdLnk sq, l member wf, IdLnk wf, true wf, Id wf